\emph{Synthetic biology} \cite{synthetic} can be defined as the design and construction of new biological parts, devices, or systems for useful purposes on strategic domains such as health, energy, or environment. Necessarily, it  raises  a number of security issues that are mainly   related  to unexpected and potentially dangerous behaviors that have not been foreseen during the design phase. Thus, as many engineering sciences addressing sensitive technology, the risk detection and prevention must be tackled at the earliest phase of the design and pursued at each stage to guarantee the safety of the products.
These matters are addressed in the ambit of \emph{toxicology}. 

Toxicology \cite{toxicology}  studies  the adverse effects of the  exposures to chemicals at  different levels of living entities:  organism, tissue, cell and intracellular molecular systems. In particular, \emph{toxicogenomics} \cite{toxicogenomics} has emerged aiming at studying the response of the  genome to toxicants: i.e. what is the toxic response to perturbations of biologic pathways. 
Pathways describe  causal chains of the cellular responses to stimuli and they are classified over the nature of the interactions: from the regulation monitoring the gene expression to the chain of signal propagation.
Most of the techniques used in toxicogenomics \cite{afshari,kavlock}  are  based on empirical analysis (biomarkers, micro arrays). 
\franck{maybe adding two lines explaining how biomarkers and micro arrays work}
We aim at providing a more systematic way of testing synthetic products. This way, instead of studying the  phenomenology of the toxic impacts, we will focus on the  causes that trigger the adverse effects on organisms. 
In particular, we believe that the main toxicity problems related to artificial pathways arise from the following two classes of situations:
\franck{ maybe you can add something here :  reformulate the problems below/adding examples ...}
\begin{enumerate}
        \item Presence/Absence of given sets of species
	\item Activation/inhibition of pathways 
\end{enumerate}
While it is clear how to connect toxicity to presence or absence of certain predefined species, the activation of undesired pathways (resp. the inhibition of desired pathways) happens when the synthetic network activates (resp. inhibits) existing/natural pathways.  Toxicity comes into play as these scenarios could break the inner equilibrium, of the organism thus causing its collapse.

\subsubsection*{Our Contribution.}
Here we propose to unify design and verification aspects by proposing a framework that by taking, for instance  a newly programmed synthetic component verifies whether the in-silico product can be safely used in in-vivo experiments. 

We assume that synthetic devices are expressed in term of pathways: i.e. reactions where the presence/absence of species at a given concentration causes the activation or inhibition of a set of signals.
The dynamics of systems is  furthermore complicated by the fact that reactions have different speeds (i.e. different durations)
\franck{maybe explain better the relation with time, what does time mean in biology?}
Our work is inspired by reaction systems as introduced in \cite{DBLP:journals/ijfcs/BrijderEMR11,DBLP:journals/tcs/EhrenfeuchtR07}. 
A reaction system is a set of \emph{reactions} $(R, I, P)$ where $R$ is the set of reactants, $I$ the set of inhibitors and $P$ the set of products, and  $R,I$ and $P$ are taken from a common set of species \res. Systems are based on three  foundational principles: 
\begin{enumerate}
 \item \label{item:react} a reaction can take place only if all the reactants involved  are available but none of the inhibitors are; 
 \item \label{item:quantity} if a species is available then a sufficient amount is present to trigger a reaction  and 
 \item species are not persistent: they become unavailable if they are not sustained by a reaction.
\end{enumerate}

From this model we retain the idea of reactions but we change considerably the semantics. The first change concerns principle \ref{item:quantity}: species are available at a given discrete expression level. The second and more fundamental change regards the introduction of discrete time constraints. Time plays a rôle in the evolution of species themselves and in the duration of reactions. 
More precisely, species are associated to  a decay time $\delta$, meaning that their  expression level diminishes with time.
This accounts for the presence of a non-specified environment that consumes and degrades species, thus allowing to abstract away from reactions that are not interesting in the specified context.
Similarly, each reaction $(R, I, P)$ is extended with a response time $\Delta$ and expression levels for all reactants and inhibitors. Thus principle \ref{item:react} is modified as follows: a reaction of response time $\Delta$ can take place only if each reactant stays  at least at a given level and each involved inhibitor is at most at a given level during the whole reaction time. 
Moreover, the expression level of  products can be augmented or diminished.
We model such systems, that we call \emph{Reaction Networks with Delays} (\rnd) into a particular form of high-level Petri nets.
The obtained network is compact and provides an intelligible graphical model of the described reactions. Moreover, the network is easy scalable: the size of the network grows linearly on the number of added species and reactions.  
Finally, by using high-level Petri nets, the model is prone to numerous extensions that are discussed in the conclusions. 

The second part of the paper is devoted to the analysis  of toxicology via \rnd networks. As the introduction of time immediately renders the state space of \rnd networks infinite, it is difficult to directly use known model checking techniques. Nevertheless,  we show that it is possible to provide a correct and complete abstraction of a \rnd network into Kripke structures. This way, by encoding properties into suitable temporal logics such as Computational Tree Logic (CTL)\cite{emerson}, we can use classical verification techniques to test them. 
We choose to present both models as the encoded Kripke structure is much more intricate, less readable, and above all not scalable and not easily extensible. Moreover, the abstraction can be automatically generate from the \rnd network. 
This way we have a complete framework where problems related to the discovering of dangerous -- toxic -- behaviors can be addressed.

\subsubsection*{Organization of the paper.} 
The paper is organized as follows: next Section \ref{sec:example} introduces our running example on blood glucose regulation. Section \ref{sec:reaction} clarifies the principles behind \rnd networks and Section \ref{sec:petri} presents \rnd semantics into  high-level Petri nets.  Then Section \ref{sec:toxic} discusses how to test toxicology properties in \rnd, recalls the definition of  CTL logic and states a proper abstraction into Kripke structures.
Finally, Section \ref{sec:concl} discusses related works and concludes with some considerations on future work.



 